Nuprl Lemma : mon_itop_split
13,42
postcript
pdf
g
:IMonoid,
a
,
b
,
c
:
.
(
a
b
)
(
b
c
)
(
E
:({
a
..
c
}
|
g
|).
(
a
j
<
c
.
E
(
j
)) = ((
a
j
<
b
.
E
(
j
)) * (
b
j
<
c
.
E
(
j
)))
|
g
|)
latex
Up
groups
1
Definitions of Statement
lb
i
<
ub
.
E
(
i
)
Definitions
lb
i
<
ub
.
E
(
i
)
Lemmas
itop
split
origin